$\forall$$T$:Type, $P$:($T$$\rightarrow\mathbb{P}$). ($\forall$$x$:$T$. Dec($P$($x$))) $\Rightarrow$ ($\forall$$L$:(\{$x$:$T$$\mid$ $P$($x$)\} List), $x$:$T$. ($x$ $\in$ $L$) $\Rightarrow$ ($x$ $\in$ $L$))